NORMALIZATION MODULE
====================

Standard: UAX #15 (Unicode Normalization Forms)
Files:    src/lingenic_text-normalization_spec.ads   (ghost specification)
          src/lingenic_text-normalization.ads        (public API)
          src/lingenic_text-normalization.adb        (implementation)


PURPOSE
-------

The Normalization module implements the four Unicode normalization forms:

  NFD   Canonical Decomposition
  NFC   Canonical Decomposition followed by Canonical Composition
  NFKD  Compatibility Decomposition
  NFKC  Compatibility Decomposition followed by Canonical Composition

Plus Quick Check and Is_Normalized queries.

Normalization is required by several higher-level algorithms (Collation
uses NFD internally; IDNA uses NFC) and is available as a standalone
transform.


GHOST SPECIFICATION (Normalization_Spec)
----------------------------------------

Package Lingenic_Text.Normalization_Spec is Pure.

Types:

  subtype CCC_Value is Natural range 0 .. 254;
    Canonical Combining Class.  0 = starter, non-zero = non-starter.

  type QC_Value is (QC_Yes, QC_No, QC_Maybe);
    Quick Check result.

  type Normalization_Form is (NFD, NFC, NFKD, NFKC);

Predicates:

  Is_Starter(CCC)              CCC = 0
  Is_Canonical(Form)           Form = NFD or Form = NFC
  Is_Compose(Form)             Form = NFC or Form = NFKC
  CCC_Ordered(A, B)            A <= B (canonical ordering)

Hangul Constants (Unicode Standard, Section 3.12):

  SBase  = 16#AC00#
  LBase  = 16#1100#
  VBase  = 16#1161#
  TBase  = 16#11A7#
  LCount = 19, VCount = 21, TCount = 28
  NCount = 588 (VCount * TCount)
  SCount = 11172 (LCount * NCount)

Hangul Predicates:

  Is_Hangul_Syllable(CP)       CP in SBase..SBase+SCount-1
  Is_Hangul_LV(CP)             LV syllable (no trailing consonant)
  Is_Hangul_L(CP)              Leading consonant jamo
  Is_Hangul_V(CP)              Vowel jamo
  Is_Hangul_T(CP)              Trailing consonant jamo


INITIALIZATION
--------------

  procedure Initialize
    (UCD_Dir : String;
     Success : out Boolean);

    Post: if Success then Initialized and Data_All_Terminal

Reads from UCD_Dir:

  UnicodeData.txt               CCC values (field 3)
                                Decomposition mappings (field 5)
  DerivedNormalizationProps.txt  Quick Check tables (NFD_QC, NFC_QC,
                                NFKD_QC, NFKC_QC)
                                Composition exclusions

Builds internal data tables:

  CCC_Table           Flat array: codepoint -> CCC_Value (0..254)
  Canon_Index/Data    Pre-expanded canonical decompositions
  Compat_Index/Data   Pre-expanded compatibility decompositions
  Comp_Index/Pairs    Composition pairs: (starter, combining) -> composite
  NFD_QC/NFC_QC/...   Quick Check tables per normalization form

Data_All_Terminal is a ghost predicate asserting that all decomposition
table entries are fully expanded (no further decomposition possible, no
Hangul syllables in the data).  True by construction: Initialize runs
Expand_Decompositions which iterates decomposition tables to fixed point.


PUBLIC API
----------

Normalize:

  procedure Normalize
    (Input  : Byte_Array;
     Form   : Normalization_Form;
     Output : in out Byte_Array;
     Last   : out Natural;
     Status : out Norm_Status);

    Pre:  Initialized, Data_All_Terminal
          Input'Length >= 1, Output'Length >= 1
          Input'Last < Positive'Last, Output'Last < Positive'Last
          Output'Length <= Max_Norm_Acc

    Post: if Status = Success then
            Last in Output'First..Output'Last
            if decompose form (NFD/NFKD):
              Ghost_Is_NFD(Output, Output'First, Last)
            if compose form (NFC/NFKC):
              Ghost_Is_NFC(Output, Output'First, Last, Is_Canonical(Form))
          else
            Last = Output'First - 1

  Status values:
    Success          Normalization completed
    Buffer_Overflow  Output buffer too small
    Invalid_Input    Input contains invalid UTF-8

  Buffer sizing:
    For NFD/NFC (canonical): Output'Length >= Input'Length * 3 is
    always sufficient (Unicode stability guarantee).
    For NFKD/NFKC: larger buffer may be needed for strings composed
    entirely of compatibility characters.

Quick_Check:

  function Quick_Check
    (Input : Byte_Array;
     Form  : Normalization_Form)
     return QC_Value;

    Returns QC_Yes if the input is definitely in the given form,
    QC_No if it definitely is not, QC_Maybe if full normalization
    is needed to determine.  NFD and NFKD never return QC_Maybe.

Is_Normalized:

  function Is_Normalized
    (Input : Byte_Array;
     Form  : Normalization_Form)
     return Boolean;

    Returns True if the input is in the given form.
    For QC_Maybe results, runs full normalization and compares.

Direct Property Access:

  Get_CCC(CP) -> CCC_Value       Canonical Combining Class
  Get_NFC_QC(CP) -> QC_Value     NFC Quick Check for single codepoint
  Get_NFKC_QC(CP) -> QC_Value    NFKC Quick Check for single codepoint


GHOST CORRECTNESS PREDICATES
-----------------------------

Ghost_Is_NFD(Output, First, Last):

  Recursive predicate checking that Output(First..Last) is in NFD:
  1. Every position contains valid UTF-8
  2. Every codepoint is fully canonically decomposed
     (Ghost_Decomp_Len(CP, True) = 0)
  3. No Hangul syllables appear (they would need decomposition)
  4. CCC values are non-decreasing within non-starter runs

Ghost_Is_NFC(Output, First, Last, Use_Canon):

  Recursive predicate checking that Output(First..Last) is in NFC/NFKC:
  1. Every position contains valid UTF-8
  2. No codepoint has Quick Check = QC_No
     (NFC_QC for canonical, NFKC_QC for compatibility)
  3. CCC values are non-decreasing within non-starter runs

Ghost Decomposition Functions:

  Ghost_Decomp_Len(CP, Use_Canon)
    Number of codepoints in CP's pre-expanded decomposition.
    Returns 0 if CP maps to itself.

  Ghost_Decomp_CP(CP, Use_Canon, Idx)
    The Idx-th codepoint in CP's decomposition (1-indexed).

  Ghost_Decomp_Out_Bytes(CP, Use_Canon)
    UTF-8 byte count for CP's NFD expansion.


NFC HELPERS AND THE DUPLICATION LEMMA
--------------------------------------

Ghost_Is_NFC_From uses non-ghost NFC_* helper functions (NFC_Valid,
NFC_Step_Length, NFC_CP) that are literal duplicates of the UTF8_Spec
ghost functions.  This duplication exists because formal function actuals
to the Text_Transform generic cannot be ghost in GNAT 15.

The equivalence is anchored by:

  procedure Lemma_NFC_Matches_UTF8_Spec(Input, Cur)
    Post: NFC_Lead_Length = UTF8_Spec.Lead_Length
          NFC_Valid = UTF8_Spec.Well_Formed_At
          NFC_Step_Length matches
          NFC_CP matches Decoded_At

The body is null (structural identity).  If either side ever drifts
from the other, this lemma fails to prove and the build breaks.


ALGORITHM OVERVIEW
------------------

NFD/NFKD:
  1. Decode input codepoint
  2. Decompose (canonical or compatibility) using pre-expanded tables
  3. For Hangul syllables, decompose algorithmically to jamo
  4. Accumulate decomposed codepoints in a segment buffer
  5. At each starter, flush the segment: sort non-starters by CCC,
     encode to output
  6. Ghost_Is_NFD_From is maintained as the loop invariant

NFC/NFKC:
  1. Perform NFD/NFKD (steps 1-5 above)
  2. During flush, apply canonical composition:
     - Find leftmost starter
     - Try composing with each non-starter (if CCC allows)
     - Composition pairs looked up in Comp_Index/Pairs table
     - Hangul L+V -> LV, LV+T -> LVT composed algorithmically
  3. Ghost_Is_NFC_From is maintained as the loop invariant

The implementation instantiates the generic Text_Transform procedure
with normalization-specific On_Codepoint and On_Finish callbacks.


CONSTANTS
---------

  Max_Decomp_Out_Bytes = 400_000   Max ghost decomposition byte count
  Max_Norm_Acc = Natural'Last / 2  Max output accumulator value
